<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">

<html>
<head>

<title>
PRISM Manual | InstallingPRISM / Instructions 
</title>

<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="keywords" content="prism, probabilistic, symbolic, model, checker, verification, birmingham, oxford, parker, norman, kwiatkowska">

<link rel="icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">
<link rel="shortcut icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">

<!--HTMLHeader--><style type='text/css'><!--
  ul, ol, pre, dl, p { margin-top:0px; margin-bottom:0px; }
  code.escaped { white-space: nowrap; }
  .vspace { margin-top:1.33em; }
  .indent { margin-left:40px; }
  .outdent { margin-left:40px; text-indent:-40px; }
  a.createlinktext { text-decoration:none; border-bottom:1px dotted gray; }
  a.createlink { text-decoration:none; position:relative; top:-0.5em;
    font-weight:bold; font-size:smaller; border-bottom:none; }
  img { border:0px; }
  .editconflict { color:green; 
  font-style:italic; margin-top:1.33em; margin-bottom:1.33em; }

  table.markup { border:2px dotted #ccf; width:90%; }
  td.markup1, td.markup2 { padding-left:10px; padding-right:10px; }
  table.vert td.markup1 { border-bottom:1px solid #ccf; }
  table.horiz td.markup1 { width:23em; border-right:1px solid #ccf; }
  table.markup caption { text-align:left; }
  div.faq p, div.faq pre { margin-left:2em; }
  div.faq p.question { margin:1em 0 0.75em 0; font-weight:bold; }
  div.faqtoc div.faq * { display:none; }
  div.faqtoc div.faq p.question 
    { display:block; font-weight:normal; margin:0.5em 0 0.5em 20px; line-height:normal; }
  div.faqtoc div.faq p.question * { display:inline; }
   
    .frame 
      { border:1px solid #cccccc; padding:4px; background-color:#f9f9f9; }
    .lfloat { float:left; margin-right:0.5em; }
    .rfloat { float:right; margin-left:0.5em; }
a.varlink { text-decoration:none; }

.sourceblocklink {
  text-align: right;
  font-size: smaller;
}
.sourceblocktext {
  padding: 0.5em;
  border: 1px solid #808080;
  color: #000000;
  background-color: #f1f0ed;
}
.sourceblocktext div {
  font-family: monospace;
  font-size: small;
  line-height: 1;
  height: 1%;
}
.sourceblocktext div.head,
.sourceblocktext div.foot {
  font: italic medium serif;
  padding: 0.5em;
}

--></style>  <meta name='robots' content='index,follow' />


<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/base.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prism.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prismmanual.css">

</head>

<body text="#000000" bgcolor="#ffffff">

<div id="layout-maincontainer">
<div id="layout-main">

<div id="prism-mainbox">

<!-- ============================================================================= -->

<!--PageHeaderFmt-->
<!--/PageHeaderFmt-->

<!--PageTitleFmt-->
  <div id="prism-man-title">
    <p><a class='wikilink' href='Instructions.html'>Installing PRISM</a> /
</p><h1>Instructions</h1>

  </div>
<!--PageText-->
<div id='wikitext'>
<h3>Prerequisites</h3>
<p>PRISM is known to run on Linux, Windows, Mac OS X and Solaris, including 64-bit variants of these operating systems.
</p>
<p class='vspace'>You will need <strong>Java</strong>, more specifically the <a class='urllink' href='http://www.oracle.com/technetwork/java/javase/downloads/index.html'>Oracle</a> (formerly Sun) version. To run binary versions of PRISM, you only need the Java Runtime Environment (JRE), not the full Java Development Kit (JDK). Currently, Java 6 (sometimes also called version 1.6) or above is required. If you don't know what version of Java you have, type <code>java -version</code> from a command prompt.
</p>
<p class='vspace'>To compile PRISM from source, you need the Java Development Kit (JDK), GNU make and a C/C++ compiler (e.g. gcc/g++). For compilation under Windows, you will need Cygwin. See below for more information.
</p>
<div class='vspace'></div><hr />
<p class='vspace'><a name='windows' id='windows'></a>
</p><h3>Installation on Windows (32-bit)</h3>
<p>To install PRISM on Windows, just run the self-extracting installer which you <a class='urllink' href='http://www.prismmodelchecker.org/download.php'>downloaded</a>. You do <strong>not</strong> need administrator privileges for this, just write-access to the directory chosen for installation.
</p>
<p class='vspace'>If requested, the installer will place shortcuts to run PRISM on the desktop and/or start menu. If not, you can run by PRISM double-clicking the file <code>xprism.bat</code> (which may just appear as <code>xprism</code>) in the <code>bin</code> folder of your PRISM folder. If nothing happens, the most likely explanation is that Java is not installed or not in your path. To check, open a command prompt window, navigate to the PRISM directory, type <code>cd bin</code>, then <code>xprism.bat</code> and examine the resulting error. If you want to create shortcuts to <code>xprism.bat</code> manually, you will find some PRISM icons in the <code>etc</code> folder.
</p>
<p class='vspace'>If you wish to use the command-line version of PRISM on Windows, open a command prompt window and type for example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock1'>
  <div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">cd "c:\Program Files\prism-4.0-win\bin"</span><br/>
<span style="font-weight:bold;">prism ..\examples\dice\dice.pm</span><br/>
</div></div>
  <div class='sourceblocklink'><a href='Instructions@action=sourceblock&amp;num=1' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>
    
<p class='vspace'>You can also edit the file <code>bin\prism.bat</code> to allow it to be run from any location. See the instructions within the file for further details.
</p>
<p class='vspace'><strong>Problems?</strong> See the section "<a class='wikilink' href='CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
</p>
<div class='vspace'></div><hr />
<p class='vspace'>
</p><h3>Installation on Windows (64-bit)</h3>
<p>PRISM is known to run on 64-bit versions of Windows. Since we currently only provide 32-bit binary versions, you will need to install and use a 32-bit, rather than 64-bit version of Java. If not, you may see strange error messages like "<code>Can't load IA 32-bit .dll on a AMD 64-bit platform</code>".
</p>
<p class='vspace'>You will probably also need to update <code>bin\xprism.bat</code> (and <code>bin\prism.bat</code>, if you use it), changing <code>javaw</code> on the last line to include the full path to the 32-bit executable.
</p>
<p class='vspace'>Other than this, installing and running PRISM is as for the 32-bit case described above.
</p>
<p class='vspace'>If this is not possible for some reason, an alternative is to build PRISM from source using Cygwin (See below).
</p>
<p class='vspace'><strong>Problems?</strong> See the section "<a class='wikilink' href='CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
</p>
<div class='vspace'></div><hr />
<p class='vspace'><a name='binaries' id='binaries'></a>
</p><h3>Installation of (non-Windows) binary versions</h3>
<p>To ensure compatibility, we recommend that you compile PRISM from source on non-Windows platforms. See below for instructions. However, we do <a class='urllink' href='http://www.prismmodelchecker.org/download.php'>provide</a> pre-compiled binary distributions for Linux (32-bit) and, depending on availability, other operating systems such as Mac OS X and Solaris.
</p>
<p class='vspace'>To install a binary distribution, unpack the tarred/zipped PRISM distribution into a suitable location, enter the directory and run the <code>install.sh</code> script, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock2'>
  <div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">gunzip prism-4.0-linux.tar.gz</span><br/>
<span style="font-weight:bold;">tar xf prism-4.0-linux.tar</span><br/>
<span style="font-weight:bold;">cd prism-4.0-linux</span><br/>
<span style="font-weight:bold;">./install.sh</span><br/>
</div></div>
  <div class='sourceblocklink'><a href='Instructions@action=sourceblock&amp;num=2' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>You do not need to be root to install PRISM. The install script simply makes some small customisations to the scripts used to launch PRISM. The PRISM distribution is self-contained and can be freely moved/renamed, however if you do so you will need to re-run <code>./install.sh</code> afterwards.
</p>
<p class='vspace'>To run PRISM, execute either the <code>xprism</code> or <code>prism</code> script (for the graphical user interface or command-line version, respectively). These can be found in the <code>bin</code> directory. These scripts are designed to be run from anywhere and you can easily create symbolic links or aliases to them. If you want icons to create desktop shortcuts to PRISM, you can find some in the <code>etc</code> directory.
</p>
<p class='vspace'><strong>Problems?</strong> See the section "<a class='wikilink' href='CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
</p>
<div class='vspace'></div><hr />
<p class='vspace'><a name='source' id='source'></a>
</p><h3>Building PRISM from source</h3>
<p>To compile PRISM form source code, you will need:
</p>
<div class='vspace'></div><ul><li>GNU make (sometimes called gmake)
</li><li>a C/C++ compiler (e.g. gcc/g++)
</li><li>The <a class='urllink' href='http://www.oracle.com/technetwork/java/javase/downloads/index.html'>Java Development Kit</a> (JDK) from Oracle (formerly Sun), version 5.0 (sometimes called 1.5) or higher
</li></ul><p class='vspace'>To check what version of Java you have, type <code>java -version</code>. To check that you have the development kit, type <code>javac</code>. If you get an error message that <code>javac</code> cannot be found, you probably do not have the JDK installed (or your path is not set up correctly).
</p>
<p class='vspace'>Hopefully, you can build PRISM simply by entering the PRISM directory and running <code>make</code>, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock3'>
  <div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">gunzip prism-4.0-src.tar.gz</span><br/>
<span style="font-weight:bold;">tar xf prism-4.0-src.tar</span><br/>
<span style="font-weight:bold;">cd prism-4.0-src</span><br/>
<span style="font-weight:bold;">make</span><br/>
</div></div>
  <div class='sourceblocklink'><a href='Instructions@action=sourceblock&amp;num=3' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>For this process to complete correctly, PRISM needs to be able to determine both the operating system you are using and the location of your Java distribution. If there is a problem with either of these, you will see an error message and will need to specify one or both of these manually, such as in these examples:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock4'>
  <div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">make OSTYPE=linux</span><br/>
<span style="font-weight:bold;">make JAVA_DIR=/usr/java/jdk1.5.0</span><br/>
<span style="font-weight:bold;">make OSTYPE=cygwin JAVA_DIR="/cygdrive/c/Program Files/Java/jdk1.5.0"</span><br/>
</div></div>
  <div class='sourceblocklink'><a href='Instructions@action=sourceblock&amp;num=4' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>Note the use of double quotes for the case where the directory contains a space. If you don't know the location of your Java installation, try typing <code>which javac</code>. If the result is e.g. <code>/usr/java/jdk1.5.0/bin/javac</code> then your Java directory is <code>/usr/java/jdk1.5.0</code>. Sometimes <code>javac</code> will be a symbolic link, in which case use "<code>ls -l</code>" to determine the actual location.
</p>
<p class='vspace'>It is also possible to to set the environment variables <code>OSTYPE</code> and <code>JAVA_DIR</code> directly or edit their values in the Makefile directly. Note that even when you specify <code>JAVA_DIR</code> explicitly (in either way), PRISM still uses the versions of <code>javac</code> (and <code>javah</code>) that are in your path so make sure this is set up correctly.
</p>
<p class='vspace'><strong>Problems?</strong> See the section "<a class='wikilink' href='CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
</p>
<div class='vspace'></div><hr />
<p class='vspace'><a name='on64bit' id='on64bit'></a>
</p><h3>Building PRISM on 64-bit machines</h3>
<p>PRISM has also been successfully compiled under Linux on a variety of 64-bit architectures. In general this should work exactly as described above. The Makefile will try to detect that you are compiling on a 64-bit machine but, if this does not work for some reason, you can override detection by setting <code>ARCH</code> to either <code>amd64</code> (for AMD/Intel 64) or <code>ia64</code> (for Itanium). For example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock5'>
  <div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">make ARCH=amd64</span><br/>
</div></div>
  <div class='sourceblocklink'><a href='Instructions@action=sourceblock&amp;num=5' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>For 64-bit Macs, see below.
</p>
<p class='vspace'><strong>Problems?</strong> See the section "<a class='wikilink' href='CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
</p>
<div class='vspace'></div><hr />
<p class='vspace'><a name='macs' id='macs'></a>
</p><h3>Building PRISM on Macs</h3>
<p>In most cases, you should be able to build PRISM from source under Mac OS X using the instructions given above. There are, however, a few known issues to be aware of.
</p>
<p class='vspace'>The most common problem is when building on recent 64-bit Macs, under which PRISM has some issues with Java. The best advice, currently, is to compile and run a 32-bit version of PRISM. To do this:
</p>
<div class='vspace'></div><ol><li>Make sure you are using a 32-bit version of Java (e.g. through "Java Preferences" under /Applications/Utilities).
<div class='vspace'></div></li><li>Make sure you have the very latest version of PRISM <a class='urllink' href='http://www.prismmodelchecker.org/download.php'>available</a>.
<div class='vspace'></div></li><li>Build PRISM (as above).
</li></ol><p class='vspace'>If this still does not work, it may be that PRISM is detecting automatically that you are on a 64-bit machine. You can override this as follows:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock6'>
  <div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">make clean_all</span><br/>
<span style="font-weight:bold;">make ARCH=</span><br/>
</div></div>
  <div class='sourceblocklink'><a href='Instructions@action=sourceblock&amp;num=6' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'><strong>Problems?</strong> See the section "<a class='wikilink' href='CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
</p>
<div class='vspace'></div><hr />
<p class='vspace'><a name='cygwin' id='cygwin'></a>
</p><h3>Building PRISM from source on Windows using Cygwin</h3>
<p>The compilation of PRISM currently relies on a Unix-like environment. On Windows, this can be achieved using the <a class='urllink' href='http://www.cygwin.com/'>Cygwin</a> development environment (or alternatively using <a class='urllink' href='http://www.mingw.org/'>MSYS</a>). Once Cygwin is installed, you can proceed as described in the previous section. Note that the PRISM compilation process uses the <a class='urllink' href='http://www.mingw.org/'>MinGW</a> libraries so that the final result is independent of Cygwin at run-time.
</p>
<p class='vspace'>One thing to note: please unzip the PRISM distribution from within Cygwin (e.g. using <code>tar xfz prism-XXX-src.tar.gz</code>). Don't use a Windows program (Winzip, etc.) since this can cause problems.
</p>
<p class='vspace'><strong>Problems?</strong> See the section "<a class='wikilink' href='CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
</p>
<div class='vspace'></div><hr />
<p class='vspace'><a name='msys' id='msys'></a>
</p><h3>Building PRISM from source on Windows using MSYS</h3>
<p>Compiling from source in <a class='urllink' href='http://www.mingw.org/'>MSYS</a> is less obvious as this environment is currently not directly supported in the makefile. Additionally, MSYS does not handle symlinks in the same way as cygwin does. The first problem is fixed by providing a OSTYPE variable to the makefile, whereas the second problem currently has to be solved manually.
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock7'>
  <div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">make OSTYPE=cygwin</span><br/>
</div></div>
  <div class='sourceblocklink'><a href='Instructions@action=sourceblock&amp;num=7' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>At some point it will fail, saying that it cannot find the CUDD library, this is due to the failing symlinks. We can solve this by means of a few commands: 
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock8'>
  <div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">cd cudd/</span><br/>
<span style="font-weight:bold;">rmdir lib/ </span><br/>
<span style="font-weight:bold;">./setup.sh</span><br/>
<span style="font-weight:bold;">cd ..</span><br/>
<span style="font-weight:bold;">make OSTYPE=cygwin </span><br/>
<span style="font-weight:bold;">./install.sh</span><br/>
</div></div>
  <div class='sourceblocklink'><a href='Instructions@action=sourceblock&amp;num=8' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'><strong>Problems?</strong> See the section "<a class='wikilink' href='CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
</p>
</div>


<!--PageFooterFmt-->
  <div id='prism-man-footer'>
  </div>
<!--/PageFooterFmt-->


<!-- ============================================================================= -->

</div> <!-- id="prism-mainbox" -->

</div> <!-- id="layout-main" -->
</div> <!-- id="layout-maincontainer" -->

<div id="layout-leftcol">
<div id="prism-navbar2">

<h3><a class='wikilink' href='../Main/Welcome.html'>PRISM Manual</a></h3>
<p><strong><a class='wikilink' href='Instructions.html'>Installing PRISM</a></strong>
</p><ul><li><a class='selflink' href='Instructions.html'>Instructions</a>
</li><li><a class='wikilink' href='CommonProblemsAndQuestions.html'>Common Problems And Questions</a>
</li></ul><p>[ <a class='wikilink' href='AllOnOnePage.html'>View all</a> ]
</p>


</div>  <!-- id="prism-navbar2" -->
</div> <!-- id="layout-leftcol" -->

</body>
</html>
